↳ Prolog
↳ PrologToPiTRSProof
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
ap1_in_aag(nil, X, X) → ap1_out_aag(nil, X, X)
ap1_in_aag(cons(H, X), Y, cons(H, Z)) → U1_aag(H, X, Y, Z, ap1_in_aag(X, Y, Z))
U1_aag(H, X, Y, Z, ap1_out_aag(X, Y, Z)) → ap1_out_aag(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
ap2_in_gga(nil, X, X) → ap2_out_gga(nil, X, X)
ap2_in_gga(cons(H, X), Y, cons(H, Z)) → U2_gga(H, X, Y, Z, ap2_in_gga(X, Y, Z))
U2_gga(H, X, Y, Z, ap2_out_gga(X, Y, Z)) → ap2_out_gga(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_ga(Zs, Ys))
U5_ga(Xs, X, Ys, perm_out_ga(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
ap1_in_aag(nil, X, X) → ap1_out_aag(nil, X, X)
ap1_in_aag(cons(H, X), Y, cons(H, Z)) → U1_aag(H, X, Y, Z, ap1_in_aag(X, Y, Z))
U1_aag(H, X, Y, Z, ap1_out_aag(X, Y, Z)) → ap1_out_aag(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
ap2_in_gga(nil, X, X) → ap2_out_gga(nil, X, X)
ap2_in_gga(cons(H, X), Y, cons(H, Z)) → U2_gga(H, X, Y, Z, ap2_in_gga(X, Y, Z))
U2_gga(H, X, Y, Z, ap2_out_gga(X, Y, Z)) → ap2_out_gga(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_ga(Zs, Ys))
U5_ga(Xs, X, Ys, perm_out_ga(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
PERM_IN_GA(Xs, cons(X, Ys)) → U3_GA(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
PERM_IN_GA(Xs, cons(X, Ys)) → AP1_IN_AAG(X1s, cons(X, X2s), Xs)
AP1_IN_AAG(cons(H, X), Y, cons(H, Z)) → U1_AAG(H, X, Y, Z, ap1_in_aag(X, Y, Z))
AP1_IN_AAG(cons(H, X), Y, cons(H, Z)) → AP1_IN_AAG(X, Y, Z)
U3_GA(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_GA(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
U3_GA(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → AP2_IN_GGA(X1s, X2s, Zs)
AP2_IN_GGA(cons(H, X), Y, cons(H, Z)) → U2_GGA(H, X, Y, Z, ap2_in_gga(X, Y, Z))
AP2_IN_GGA(cons(H, X), Y, cons(H, Z)) → AP2_IN_GGA(X, Y, Z)
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → U5_GA(Xs, X, Ys, perm_in_ga(Zs, Ys))
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → PERM_IN_GA(Zs, Ys)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
ap1_in_aag(nil, X, X) → ap1_out_aag(nil, X, X)
ap1_in_aag(cons(H, X), Y, cons(H, Z)) → U1_aag(H, X, Y, Z, ap1_in_aag(X, Y, Z))
U1_aag(H, X, Y, Z, ap1_out_aag(X, Y, Z)) → ap1_out_aag(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
ap2_in_gga(nil, X, X) → ap2_out_gga(nil, X, X)
ap2_in_gga(cons(H, X), Y, cons(H, Z)) → U2_gga(H, X, Y, Z, ap2_in_gga(X, Y, Z))
U2_gga(H, X, Y, Z, ap2_out_gga(X, Y, Z)) → ap2_out_gga(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_ga(Zs, Ys))
U5_ga(Xs, X, Ys, perm_out_ga(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
PERM_IN_GA(Xs, cons(X, Ys)) → U3_GA(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
PERM_IN_GA(Xs, cons(X, Ys)) → AP1_IN_AAG(X1s, cons(X, X2s), Xs)
AP1_IN_AAG(cons(H, X), Y, cons(H, Z)) → U1_AAG(H, X, Y, Z, ap1_in_aag(X, Y, Z))
AP1_IN_AAG(cons(H, X), Y, cons(H, Z)) → AP1_IN_AAG(X, Y, Z)
U3_GA(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_GA(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
U3_GA(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → AP2_IN_GGA(X1s, X2s, Zs)
AP2_IN_GGA(cons(H, X), Y, cons(H, Z)) → U2_GGA(H, X, Y, Z, ap2_in_gga(X, Y, Z))
AP2_IN_GGA(cons(H, X), Y, cons(H, Z)) → AP2_IN_GGA(X, Y, Z)
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → U5_GA(Xs, X, Ys, perm_in_ga(Zs, Ys))
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → PERM_IN_GA(Zs, Ys)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
ap1_in_aag(nil, X, X) → ap1_out_aag(nil, X, X)
ap1_in_aag(cons(H, X), Y, cons(H, Z)) → U1_aag(H, X, Y, Z, ap1_in_aag(X, Y, Z))
U1_aag(H, X, Y, Z, ap1_out_aag(X, Y, Z)) → ap1_out_aag(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
ap2_in_gga(nil, X, X) → ap2_out_gga(nil, X, X)
ap2_in_gga(cons(H, X), Y, cons(H, Z)) → U2_gga(H, X, Y, Z, ap2_in_gga(X, Y, Z))
U2_gga(H, X, Y, Z, ap2_out_gga(X, Y, Z)) → ap2_out_gga(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_ga(Zs, Ys))
U5_ga(Xs, X, Ys, perm_out_ga(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
AP2_IN_GGA(cons(H, X), Y, cons(H, Z)) → AP2_IN_GGA(X, Y, Z)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
ap1_in_aag(nil, X, X) → ap1_out_aag(nil, X, X)
ap1_in_aag(cons(H, X), Y, cons(H, Z)) → U1_aag(H, X, Y, Z, ap1_in_aag(X, Y, Z))
U1_aag(H, X, Y, Z, ap1_out_aag(X, Y, Z)) → ap1_out_aag(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
ap2_in_gga(nil, X, X) → ap2_out_gga(nil, X, X)
ap2_in_gga(cons(H, X), Y, cons(H, Z)) → U2_gga(H, X, Y, Z, ap2_in_gga(X, Y, Z))
U2_gga(H, X, Y, Z, ap2_out_gga(X, Y, Z)) → ap2_out_gga(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_ga(Zs, Ys))
U5_ga(Xs, X, Ys, perm_out_ga(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
AP2_IN_GGA(cons(H, X), Y, cons(H, Z)) → AP2_IN_GGA(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
AP2_IN_GGA(cons(X), Y) → AP2_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
AP1_IN_AAG(cons(H, X), Y, cons(H, Z)) → AP1_IN_AAG(X, Y, Z)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
ap1_in_aag(nil, X, X) → ap1_out_aag(nil, X, X)
ap1_in_aag(cons(H, X), Y, cons(H, Z)) → U1_aag(H, X, Y, Z, ap1_in_aag(X, Y, Z))
U1_aag(H, X, Y, Z, ap1_out_aag(X, Y, Z)) → ap1_out_aag(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
ap2_in_gga(nil, X, X) → ap2_out_gga(nil, X, X)
ap2_in_gga(cons(H, X), Y, cons(H, Z)) → U2_gga(H, X, Y, Z, ap2_in_gga(X, Y, Z))
U2_gga(H, X, Y, Z, ap2_out_gga(X, Y, Z)) → ap2_out_gga(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_ga(Zs, Ys))
U5_ga(Xs, X, Ys, perm_out_ga(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
AP1_IN_AAG(cons(H, X), Y, cons(H, Z)) → AP1_IN_AAG(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
AP1_IN_AAG(cons(Z)) → AP1_IN_AAG(Z)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
PERM_IN_GA(Xs, cons(X, Ys)) → U3_GA(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → PERM_IN_GA(Zs, Ys)
U3_GA(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_GA(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
ap1_in_aag(nil, X, X) → ap1_out_aag(nil, X, X)
ap1_in_aag(cons(H, X), Y, cons(H, Z)) → U1_aag(H, X, Y, Z, ap1_in_aag(X, Y, Z))
U1_aag(H, X, Y, Z, ap1_out_aag(X, Y, Z)) → ap1_out_aag(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
ap2_in_gga(nil, X, X) → ap2_out_gga(nil, X, X)
ap2_in_gga(cons(H, X), Y, cons(H, Z)) → U2_gga(H, X, Y, Z, ap2_in_gga(X, Y, Z))
U2_gga(H, X, Y, Z, ap2_out_gga(X, Y, Z)) → ap2_out_gga(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_ga(Zs, Ys))
U5_ga(Xs, X, Ys, perm_out_ga(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
PERM_IN_GA(Xs, cons(X, Ys)) → U3_GA(Xs, X, Ys, ap1_in_aag(X1s, cons(X, X2s), Xs))
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gga(X1s, X2s, Zs)) → PERM_IN_GA(Zs, Ys)
U3_GA(Xs, X, Ys, ap1_out_aag(X1s, cons(X, X2s), Xs)) → U4_GA(Xs, X, Ys, X1s, X2s, ap2_in_gga(X1s, X2s, Zs))
ap1_in_aag(nil, X, X) → ap1_out_aag(nil, X, X)
ap1_in_aag(cons(H, X), Y, cons(H, Z)) → U1_aag(H, X, Y, Z, ap1_in_aag(X, Y, Z))
ap2_in_gga(nil, X, X) → ap2_out_gga(nil, X, X)
ap2_in_gga(cons(H, X), Y, cons(H, Z)) → U2_gga(H, X, Y, Z, ap2_in_gga(X, Y, Z))
U1_aag(H, X, Y, Z, ap1_out_aag(X, Y, Z)) → ap1_out_aag(cons(H, X), Y, cons(H, Z))
U2_gga(H, X, Y, Z, ap2_out_gga(X, Y, Z)) → ap2_out_gga(cons(H, X), Y, cons(H, Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
U3_GA(ap1_out_aag(X1s, cons(X2s))) → U4_GA(ap2_in_gga(X1s, X2s))
U4_GA(ap2_out_gga(Zs)) → PERM_IN_GA(Zs)
PERM_IN_GA(Xs) → U3_GA(ap1_in_aag(Xs))
ap1_in_aag(X) → ap1_out_aag(nil, X)
ap1_in_aag(cons(Z)) → U1_aag(ap1_in_aag(Z))
ap2_in_gga(nil, X) → ap2_out_gga(X)
ap2_in_gga(cons(X), Y) → U2_gga(ap2_in_gga(X, Y))
U1_aag(ap1_out_aag(X, Y)) → ap1_out_aag(cons(X), Y)
U2_gga(ap2_out_gga(Z)) → ap2_out_gga(cons(Z))
ap1_in_aag(x0)
ap2_in_gga(x0, x1)
U1_aag(x0)
U2_gga(x0)
U3_GA(ap1_out_aag(X1s, cons(X2s))) → U4_GA(ap2_in_gga(X1s, X2s))
POL(PERM_IN_GA(x1)) = 2·x1
POL(U1_aag(x1)) = 2 + x1
POL(U2_gga(x1)) = 1 + x1
POL(U3_GA(x1)) = x1
POL(U4_GA(x1)) = 2·x1
POL(ap1_in_aag(x1)) = 2·x1
POL(ap1_out_aag(x1, x2)) = 2·x1 + 2·x2
POL(ap2_in_gga(x1, x2)) = x1 + x2
POL(ap2_out_gga(x1)) = x1
POL(cons(x1)) = 1 + x1
POL(nil) = 0
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
U4_GA(ap2_out_gga(Zs)) → PERM_IN_GA(Zs)
PERM_IN_GA(Xs) → U3_GA(ap1_in_aag(Xs))
ap1_in_aag(X) → ap1_out_aag(nil, X)
ap1_in_aag(cons(Z)) → U1_aag(ap1_in_aag(Z))
ap2_in_gga(nil, X) → ap2_out_gga(X)
ap2_in_gga(cons(X), Y) → U2_gga(ap2_in_gga(X, Y))
U1_aag(ap1_out_aag(X, Y)) → ap1_out_aag(cons(X), Y)
U2_gga(ap2_out_gga(Z)) → ap2_out_gga(cons(Z))
ap1_in_aag(x0)
ap2_in_gga(x0, x1)
U1_aag(x0)
U2_gga(x0)